Metamath Blueprint : AKS (PRIMES is in P)

Theorem aksthr

Metamath Blueprints

Triangle Congruences
Derivative of real logarithm (iset)
AKS (PRIMES is in P)
- akslb
- aks61
- aks61c4
- aks61c3
- aks61c1
- rhmextex
- intro2
- aks61c2
- lcmineqlem
- cl3
- odrlblem
- claim2p1
- aks10kbnd
- aks61c7
- aks61c5
- defintrospective
- taylconcavebnd
- aks61c6
- aksthr
- intro1
- aks22
- aksth

Status:

Draft

Reference:

Lemma 2.1 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf

Simpler direction of the AKS theorem: